Nuprl Lemma : R-sub-Rlist
11,40
postcript
pdf
L
:(Realizer List),
A
:Realizer. (
A
L
)
A
(
L
)
latex
Definitions
P
&
Q
,
x
.
t
(
x
)
,
,
P
Q
,
P
Q
,
P
Q
,
Y
,
reduce(
f
;
k
;
as
)
,
(
L
)
,
P
Q
,
t
T
,
x
:
A
.
B
(
x
)
,
{
T
}
,
x
(
s
)
,
||
as
||
,
A
c
B
,
x
:
A
.
B
(
x
)
,
(
x
l
)
Lemmas
R-sub-lemma1
,
R-sub-plus-left
,
cons
member
,
implies
functionality
wrt
iff
,
Rlist
wf
,
Rplus
wf
,
R-sub
wf
,
all
functionality
wrt
iff
,
l
member
wf
,
es
realizer
wf
origin
L:(Realizer List), A:Realizer. (A 
L) 
A 
(L) L:(Realizer List), A:Realizer. (A L) A (L) 
x. t(x)
Q
Q Q(L) Q Tx:A. B(x)
B
x:A. B(x) l)